Step of Proof: complete_nat_ind_with_y 9,38
Inference at * 1 1 
Iof proof for Lemma complete nat ind with y:

.....subterm..... T:t1:n

1. P : {k}
2. g : i:. (j:i. P(j))  P(i)
  Y(f,x. g(x,f))  (i:. P(i)) 
latex
 by Assert Y(f,x. g(x,f))  !Void()!Void() 
latex

 1: .....assertion..... NILNIL

 1:   Y(f,x. g(x,f))  !Void()!Void()
 2: 

 2: 3. Y(f,x. g(x,f))  !Void()!Void()
 2:   Y(f,x. g(x,f))  (i:. P(i))
 .

Definitionst  T, x:AB(x), !Void(), Y, x.A(x), f(a)

origin